Left Termination of the query pattern
shanoi(g,g,g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 186 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 168 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES

(0) Obligation:

Clauses:

shanoi(s(0), A, B, C, .(mv(A, C), [])).
shanoi(s(s(X)), A, B, C, M) :- ','(eq(N1, s(X)), ','(shanoi(N1, A, C, B, M1), ','(shanoi(N1, B, A, C, M2), ','(append(M1, .(mv(A, C), []), T), append(T, M2, M))))).
append([], L, L).
append(.(H, L), L1, .(H, R)) :- append(L, L1, R).
eq(X, X).

Query: shanoi(g,g,g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

shanoiA(s(X1), X2, X3, X4, X5) :- shanoiA(X1, X2, X4, X3, X6).
shanoiA(s(X1), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), shanoiA(X1, X3, X2, X4, X7)).
shanoiA(s(X1), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), ','(shanoicA(X1, X3, X2, X4, X7), appendB(X6, .(mv(X2, X4), []), X8))).
shanoiA(s(X1), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), ','(shanoicA(X1, X3, X2, X4, X7), ','(appendcB(X6, .(mv(X2, X4), []), X8), appendB(X8, X7, X5)))).
appendB(.(X1, X2), X3, .(X1, X4)) :- appendB(X2, X3, X4).
appendC(.(X1, X2), X3, .(X1, X4)) :- appendC(X2, X3, X4).
shanoiD(s(s(X1)), X2, X3, X4, X5) :- shanoiA(X1, X2, X4, X3, X6).
shanoiD(s(s(X1)), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), shanoiA(X1, X3, X2, X4, X7)).
shanoiD(s(s(X1)), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), ','(shanoicA(X1, X3, X2, X4, X7), appendC(X6, .(mv(X2, X4), []), X8))).
shanoiD(s(s(X1)), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), ','(shanoicA(X1, X3, X2, X4, X7), ','(appendcC(X6, .(mv(X2, X4), []), X8), appendC(X8, X7, X5)))).

Clauses:

shanoicA(0, X1, X2, X3, .(mv(X1, X3), [])).
shanoicA(s(X1), X2, X3, X4, X5) :- ','(shanoicA(X1, X2, X4, X3, X6), ','(shanoicA(X1, X3, X2, X4, X7), ','(appendcB(X6, .(mv(X2, X4), []), X8), appendcB(X8, X7, X5)))).
appendcB([], X1, X1).
appendcB(.(X1, X2), X3, .(X1, X4)) :- appendcB(X2, X3, X4).
appendcC([], X1, X1).
appendcC(.(X1, X2), X3, .(X1, X4)) :- appendcC(X2, X3, X4).

Afs:

shanoiD(x1, x2, x3, x4, x5)  =  shanoiD(x1, x2, x3, x4)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
shanoiD_in: (b,b,b,b,f)
shanoiA_in: (b,b,b,b,f)
shanoicA_in: (b,b,b,b,f)
appendcB_in: (b,b,f)
appendB_in: (b,b,f)
appendC_in: (b,b,f)
appendcC_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SHANOID_IN_GGGGA(s(s(X1)), X2, X3, X4, X5) → U10_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X2, X4, X3, X6))
SHANOID_IN_GGGGA(s(s(X1)), X2, X3, X4, X5) → SHANOIA_IN_GGGGA(X1, X2, X4, X3, X6)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → U1_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X2, X4, X3, X6))
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → SHANOIA_IN_GGGGA(X1, X2, X4, X3, X6)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U3_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X3, X2, X4, X7))
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4, X7)
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U5_GGGGA(X1, X2, X3, X4, X5, appendB_in_gga(X6, .(mv(X2, X4), []), X8))
U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → APPENDB_IN_GGA(X6, .(mv(X2, X4), []), X8)
APPENDB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U8_GGA(X1, X2, X3, X4, appendB_in_gga(X2, X3, X4))
APPENDB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDB_IN_GGA(X2, X3, X4)
U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U6_GGGGA(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
U6_GGGGA(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U7_GGGGA(X1, X2, X3, X4, X5, appendB_in_gga(X8, X7, X5))
U6_GGGGA(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → APPENDB_IN_GGA(X8, X7, X5)
SHANOID_IN_GGGGA(s(s(X1)), X2, X3, X4, X5) → U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U12_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X3, X2, X4, X7))
U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4, X7)
U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U14_GGGGA(X1, X2, X3, X4, X5, appendC_in_gga(X6, .(mv(X2, X4), []), X8))
U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → APPENDC_IN_GGA(X6, .(mv(X2, X4), []), X8)
APPENDC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U9_GGA(X1, X2, X3, X4, appendC_in_gga(X2, X3, X4))
APPENDC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)
U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U15_GGGGA(X1, X2, X3, X4, X5, X7, appendcC_in_gga(X6, .(mv(X2, X4), []), X8))
U15_GGGGA(X1, X2, X3, X4, X5, X7, appendcC_out_gga(X6, .(mv(X2, X4), []), X8)) → U16_GGGGA(X1, X2, X3, X4, X5, appendC_in_gga(X8, X7, X5))
U15_GGGGA(X1, X2, X3, X4, X5, X7, appendcC_out_gga(X6, .(mv(X2, X4), []), X8)) → APPENDC_IN_GGA(X8, X7, X5)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3, .(mv(X1, X3), [])) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4, X5) → U18_gggga(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U18_gggga(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
appendcB_in_gga([], X1, X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U22_gga(X1, X2, X3, X4, appendcB_in_gga(X2, X3, X4))
U22_gga(X1, X2, X3, X4, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))
U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, X5, appendcB_in_gga(X8, X7, X5))
U21_gggga(X1, X2, X3, X4, X5, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
appendcC_in_gga([], X1, X1) → appendcC_out_gga([], X1, X1)
appendcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U23_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U23_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
shanoiA_in_gggga(x1, x2, x3, x4, x5)  =  shanoiA_in_gggga(x1, x2, x3, x4)
shanoicA_in_gggga(x1, x2, x3, x4, x5)  =  shanoicA_in_gggga(x1, x2, x3, x4)
0  =  0
shanoicA_out_gggga(x1, x2, x3, x4, x5)  =  shanoicA_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6)  =  U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U20_gggga(x1, x2, x3, x4, x6, x7)
appendcB_in_gga(x1, x2, x3)  =  appendcB_in_gga(x1, x2)
[]  =  []
appendcB_out_gga(x1, x2, x3)  =  appendcB_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
mv(x1, x2)  =  mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
appendB_in_gga(x1, x2, x3)  =  appendB_in_gga(x1, x2)
appendC_in_gga(x1, x2, x3)  =  appendC_in_gga(x1, x2)
appendcC_in_gga(x1, x2, x3)  =  appendcC_in_gga(x1, x2)
appendcC_out_gga(x1, x2, x3)  =  appendcC_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x2, x3, x5)
SHANOID_IN_GGGGA(x1, x2, x3, x4, x5)  =  SHANOID_IN_GGGGA(x1, x2, x3, x4)
U10_GGGGA(x1, x2, x3, x4, x5, x6)  =  U10_GGGGA(x1, x2, x3, x4, x6)
SHANOIA_IN_GGGGA(x1, x2, x3, x4, x5)  =  SHANOIA_IN_GGGGA(x1, x2, x3, x4)
U1_GGGGA(x1, x2, x3, x4, x5, x6)  =  U1_GGGGA(x1, x2, x3, x4, x6)
U2_GGGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGGA(x1, x2, x3, x4, x6)
U3_GGGGA(x1, x2, x3, x4, x5, x6)  =  U3_GGGGA(x1, x2, x3, x4, x6)
U4_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GGGGA(x1, x2, x3, x4, x6, x7)
U5_GGGGA(x1, x2, x3, x4, x5, x6)  =  U5_GGGGA(x1, x2, x3, x4, x6)
APPENDB_IN_GGA(x1, x2, x3)  =  APPENDB_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5)  =  U8_GGA(x1, x2, x3, x5)
U6_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GGGGA(x1, x2, x3, x4, x6, x7)
U7_GGGGA(x1, x2, x3, x4, x5, x6)  =  U7_GGGGA(x1, x2, x3, x4, x6)
U11_GGGGA(x1, x2, x3, x4, x5, x6)  =  U11_GGGGA(x1, x2, x3, x4, x6)
U12_GGGGA(x1, x2, x3, x4, x5, x6)  =  U12_GGGGA(x1, x2, x3, x4, x6)
U13_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GGGGA(x1, x2, x3, x4, x6, x7)
U14_GGGGA(x1, x2, x3, x4, x5, x6)  =  U14_GGGGA(x1, x2, x3, x4, x6)
APPENDC_IN_GGA(x1, x2, x3)  =  APPENDC_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5)  =  U9_GGA(x1, x2, x3, x5)
U15_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U15_GGGGA(x1, x2, x3, x4, x6, x7)
U16_GGGGA(x1, x2, x3, x4, x5, x6)  =  U16_GGGGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SHANOID_IN_GGGGA(s(s(X1)), X2, X3, X4, X5) → U10_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X2, X4, X3, X6))
SHANOID_IN_GGGGA(s(s(X1)), X2, X3, X4, X5) → SHANOIA_IN_GGGGA(X1, X2, X4, X3, X6)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → U1_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X2, X4, X3, X6))
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → SHANOIA_IN_GGGGA(X1, X2, X4, X3, X6)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U3_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X3, X2, X4, X7))
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4, X7)
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U5_GGGGA(X1, X2, X3, X4, X5, appendB_in_gga(X6, .(mv(X2, X4), []), X8))
U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → APPENDB_IN_GGA(X6, .(mv(X2, X4), []), X8)
APPENDB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U8_GGA(X1, X2, X3, X4, appendB_in_gga(X2, X3, X4))
APPENDB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDB_IN_GGA(X2, X3, X4)
U4_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U6_GGGGA(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
U6_GGGGA(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U7_GGGGA(X1, X2, X3, X4, X5, appendB_in_gga(X8, X7, X5))
U6_GGGGA(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → APPENDB_IN_GGA(X8, X7, X5)
SHANOID_IN_GGGGA(s(s(X1)), X2, X3, X4, X5) → U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U12_GGGGA(X1, X2, X3, X4, X5, shanoiA_in_gggga(X1, X3, X2, X4, X7))
U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4, X7)
U11_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U14_GGGGA(X1, X2, X3, X4, X5, appendC_in_gga(X6, .(mv(X2, X4), []), X8))
U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → APPENDC_IN_GGA(X6, .(mv(X2, X4), []), X8)
APPENDC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U9_GGA(X1, X2, X3, X4, appendC_in_gga(X2, X3, X4))
APPENDC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)
U13_GGGGA(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U15_GGGGA(X1, X2, X3, X4, X5, X7, appendcC_in_gga(X6, .(mv(X2, X4), []), X8))
U15_GGGGA(X1, X2, X3, X4, X5, X7, appendcC_out_gga(X6, .(mv(X2, X4), []), X8)) → U16_GGGGA(X1, X2, X3, X4, X5, appendC_in_gga(X8, X7, X5))
U15_GGGGA(X1, X2, X3, X4, X5, X7, appendcC_out_gga(X6, .(mv(X2, X4), []), X8)) → APPENDC_IN_GGA(X8, X7, X5)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3, .(mv(X1, X3), [])) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4, X5) → U18_gggga(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U18_gggga(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
appendcB_in_gga([], X1, X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U22_gga(X1, X2, X3, X4, appendcB_in_gga(X2, X3, X4))
U22_gga(X1, X2, X3, X4, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))
U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, X5, appendcB_in_gga(X8, X7, X5))
U21_gggga(X1, X2, X3, X4, X5, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
appendcC_in_gga([], X1, X1) → appendcC_out_gga([], X1, X1)
appendcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U23_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U23_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
shanoiA_in_gggga(x1, x2, x3, x4, x5)  =  shanoiA_in_gggga(x1, x2, x3, x4)
shanoicA_in_gggga(x1, x2, x3, x4, x5)  =  shanoicA_in_gggga(x1, x2, x3, x4)
0  =  0
shanoicA_out_gggga(x1, x2, x3, x4, x5)  =  shanoicA_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6)  =  U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U20_gggga(x1, x2, x3, x4, x6, x7)
appendcB_in_gga(x1, x2, x3)  =  appendcB_in_gga(x1, x2)
[]  =  []
appendcB_out_gga(x1, x2, x3)  =  appendcB_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
mv(x1, x2)  =  mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
appendB_in_gga(x1, x2, x3)  =  appendB_in_gga(x1, x2)
appendC_in_gga(x1, x2, x3)  =  appendC_in_gga(x1, x2)
appendcC_in_gga(x1, x2, x3)  =  appendcC_in_gga(x1, x2)
appendcC_out_gga(x1, x2, x3)  =  appendcC_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x2, x3, x5)
SHANOID_IN_GGGGA(x1, x2, x3, x4, x5)  =  SHANOID_IN_GGGGA(x1, x2, x3, x4)
U10_GGGGA(x1, x2, x3, x4, x5, x6)  =  U10_GGGGA(x1, x2, x3, x4, x6)
SHANOIA_IN_GGGGA(x1, x2, x3, x4, x5)  =  SHANOIA_IN_GGGGA(x1, x2, x3, x4)
U1_GGGGA(x1, x2, x3, x4, x5, x6)  =  U1_GGGGA(x1, x2, x3, x4, x6)
U2_GGGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGGA(x1, x2, x3, x4, x6)
U3_GGGGA(x1, x2, x3, x4, x5, x6)  =  U3_GGGGA(x1, x2, x3, x4, x6)
U4_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GGGGA(x1, x2, x3, x4, x6, x7)
U5_GGGGA(x1, x2, x3, x4, x5, x6)  =  U5_GGGGA(x1, x2, x3, x4, x6)
APPENDB_IN_GGA(x1, x2, x3)  =  APPENDB_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5)  =  U8_GGA(x1, x2, x3, x5)
U6_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GGGGA(x1, x2, x3, x4, x6, x7)
U7_GGGGA(x1, x2, x3, x4, x5, x6)  =  U7_GGGGA(x1, x2, x3, x4, x6)
U11_GGGGA(x1, x2, x3, x4, x5, x6)  =  U11_GGGGA(x1, x2, x3, x4, x6)
U12_GGGGA(x1, x2, x3, x4, x5, x6)  =  U12_GGGGA(x1, x2, x3, x4, x6)
U13_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GGGGA(x1, x2, x3, x4, x6, x7)
U14_GGGGA(x1, x2, x3, x4, x5, x6)  =  U14_GGGGA(x1, x2, x3, x4, x6)
APPENDC_IN_GGA(x1, x2, x3)  =  APPENDC_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5)  =  U9_GGA(x1, x2, x3, x5)
U15_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U15_GGGGA(x1, x2, x3, x4, x6, x7)
U16_GGGGA(x1, x2, x3, x4, x5, x6)  =  U16_GGGGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 21 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3, .(mv(X1, X3), [])) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4, X5) → U18_gggga(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U18_gggga(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
appendcB_in_gga([], X1, X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U22_gga(X1, X2, X3, X4, appendcB_in_gga(X2, X3, X4))
U22_gga(X1, X2, X3, X4, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))
U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, X5, appendcB_in_gga(X8, X7, X5))
U21_gggga(X1, X2, X3, X4, X5, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
appendcC_in_gga([], X1, X1) → appendcC_out_gga([], X1, X1)
appendcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U23_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U23_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
shanoicA_in_gggga(x1, x2, x3, x4, x5)  =  shanoicA_in_gggga(x1, x2, x3, x4)
0  =  0
shanoicA_out_gggga(x1, x2, x3, x4, x5)  =  shanoicA_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6)  =  U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U20_gggga(x1, x2, x3, x4, x6, x7)
appendcB_in_gga(x1, x2, x3)  =  appendcB_in_gga(x1, x2)
[]  =  []
appendcB_out_gga(x1, x2, x3)  =  appendcB_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
mv(x1, x2)  =  mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
appendcC_in_gga(x1, x2, x3)  =  appendcC_in_gga(x1, x2)
appendcC_out_gga(x1, x2, x3)  =  appendcC_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x2, x3, x5)
APPENDC_IN_GGA(x1, x2, x3)  =  APPENDC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPENDC_IN_GGA(x1, x2, x3)  =  APPENDC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPENDC_IN_GGA(.(X1, X2), X3) → APPENDC_IN_GGA(X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPENDC_IN_GGA(.(X1, X2), X3) → APPENDC_IN_GGA(X2, X3)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDB_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3, .(mv(X1, X3), [])) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4, X5) → U18_gggga(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U18_gggga(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
appendcB_in_gga([], X1, X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U22_gga(X1, X2, X3, X4, appendcB_in_gga(X2, X3, X4))
U22_gga(X1, X2, X3, X4, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))
U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, X5, appendcB_in_gga(X8, X7, X5))
U21_gggga(X1, X2, X3, X4, X5, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
appendcC_in_gga([], X1, X1) → appendcC_out_gga([], X1, X1)
appendcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U23_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U23_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
shanoicA_in_gggga(x1, x2, x3, x4, x5)  =  shanoicA_in_gggga(x1, x2, x3, x4)
0  =  0
shanoicA_out_gggga(x1, x2, x3, x4, x5)  =  shanoicA_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6)  =  U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U20_gggga(x1, x2, x3, x4, x6, x7)
appendcB_in_gga(x1, x2, x3)  =  appendcB_in_gga(x1, x2)
[]  =  []
appendcB_out_gga(x1, x2, x3)  =  appendcB_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
mv(x1, x2)  =  mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
appendcC_in_gga(x1, x2, x3)  =  appendcC_in_gga(x1, x2)
appendcC_out_gga(x1, x2, x3)  =  appendcC_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x2, x3, x5)
APPENDB_IN_GGA(x1, x2, x3)  =  APPENDB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDB_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPENDB_IN_GGA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPENDB_IN_GGA(x1, x2, x3)  =  APPENDB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPENDB_IN_GGA(.(X1, X2), X3) → APPENDB_IN_GGA(X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPENDB_IN_GGA(.(X1, X2), X3) → APPENDB_IN_GGA(X2, X3)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4, X7)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → SHANOIA_IN_GGGGA(X1, X2, X4, X3, X6)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3, .(mv(X1, X3), [])) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4, X5) → U18_gggga(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U18_gggga(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
appendcB_in_gga([], X1, X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U22_gga(X1, X2, X3, X4, appendcB_in_gga(X2, X3, X4))
U22_gga(X1, X2, X3, X4, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))
U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, X5, appendcB_in_gga(X8, X7, X5))
U21_gggga(X1, X2, X3, X4, X5, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
appendcC_in_gga([], X1, X1) → appendcC_out_gga([], X1, X1)
appendcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U23_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U23_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
shanoicA_in_gggga(x1, x2, x3, x4, x5)  =  shanoicA_in_gggga(x1, x2, x3, x4)
0  =  0
shanoicA_out_gggga(x1, x2, x3, x4, x5)  =  shanoicA_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6)  =  U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U20_gggga(x1, x2, x3, x4, x6, x7)
appendcB_in_gga(x1, x2, x3)  =  appendcB_in_gga(x1, x2)
[]  =  []
appendcB_out_gga(x1, x2, x3)  =  appendcB_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
mv(x1, x2)  =  mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
appendcC_in_gga(x1, x2, x3)  =  appendcC_in_gga(x1, x2)
appendcC_out_gga(x1, x2, x3)  =  appendcC_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x2, x3, x5)
SHANOIA_IN_GGGGA(x1, x2, x3, x4, x5)  =  SHANOIA_IN_GGGGA(x1, x2, x3, x4)
U2_GGGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U2_GGGGA(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4, X7)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4, X5) → SHANOIA_IN_GGGGA(X1, X2, X4, X3, X6)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3, .(mv(X1, X3), [])) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4, X5) → U18_gggga(X1, X2, X3, X4, X5, shanoicA_in_gggga(X1, X2, X4, X3, X6))
U18_gggga(X1, X2, X3, X4, X5, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_in_gggga(X1, X3, X2, X4, X7))
U19_gggga(X1, X2, X3, X4, X5, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_in_gga(X6, .(mv(X2, X4), []), X8))
U20_gggga(X1, X2, X3, X4, X5, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, X5, appendcB_in_gga(X8, X7, X5))
appendcB_in_gga([], X1, X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3, .(X1, X4)) → U22_gga(X1, X2, X3, X4, appendcB_in_gga(X2, X3, X4))
U21_gggga(X1, X2, X3, X4, X5, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
U22_gga(X1, X2, X3, X4, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
shanoicA_in_gggga(x1, x2, x3, x4, x5)  =  shanoicA_in_gggga(x1, x2, x3, x4)
0  =  0
shanoicA_out_gggga(x1, x2, x3, x4, x5)  =  shanoicA_out_gggga(x1, x2, x3, x4, x5)
U18_gggga(x1, x2, x3, x4, x5, x6)  =  U18_gggga(x1, x2, x3, x4, x6)
U19_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U19_gggga(x1, x2, x3, x4, x6, x7)
U20_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U20_gggga(x1, x2, x3, x4, x6, x7)
appendcB_in_gga(x1, x2, x3)  =  appendcB_in_gga(x1, x2)
[]  =  []
appendcB_out_gga(x1, x2, x3)  =  appendcB_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
mv(x1, x2)  =  mv(x1, x2)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
SHANOIA_IN_GGGGA(x1, x2, x3, x4, x5)  =  SHANOIA_IN_GGGGA(x1, x2, x3, x4)
U2_GGGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SHANOIA_IN_GGGGA(s(X1), X2, X3, X4) → U2_GGGGA(X1, X2, X3, X4, shanoicA_in_gggga(X1, X2, X4, X3))
U2_GGGGA(X1, X2, X3, X4, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4)
SHANOIA_IN_GGGGA(s(X1), X2, X3, X4) → SHANOIA_IN_GGGGA(X1, X2, X4, X3)

The TRS R consists of the following rules:

shanoicA_in_gggga(0, X1, X2, X3) → shanoicA_out_gggga(0, X1, X2, X3, .(mv(X1, X3), []))
shanoicA_in_gggga(s(X1), X2, X3, X4) → U18_gggga(X1, X2, X3, X4, shanoicA_in_gggga(X1, X2, X4, X3))
U18_gggga(X1, X2, X3, X4, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → U19_gggga(X1, X2, X3, X4, X6, shanoicA_in_gggga(X1, X3, X2, X4))
U19_gggga(X1, X2, X3, X4, X6, shanoicA_out_gggga(X1, X3, X2, X4, X7)) → U20_gggga(X1, X2, X3, X4, X7, appendcB_in_gga(X6, .(mv(X2, X4), [])))
U20_gggga(X1, X2, X3, X4, X7, appendcB_out_gga(X6, .(mv(X2, X4), []), X8)) → U21_gggga(X1, X2, X3, X4, appendcB_in_gga(X8, X7))
appendcB_in_gga([], X1) → appendcB_out_gga([], X1, X1)
appendcB_in_gga(.(X1, X2), X3) → U22_gga(X1, X2, X3, appendcB_in_gga(X2, X3))
U21_gggga(X1, X2, X3, X4, appendcB_out_gga(X8, X7, X5)) → shanoicA_out_gggga(s(X1), X2, X3, X4, X5)
U22_gga(X1, X2, X3, appendcB_out_gga(X2, X3, X4)) → appendcB_out_gga(.(X1, X2), X3, .(X1, X4))

The set Q consists of the following terms:

shanoicA_in_gggga(x0, x1, x2, x3)
U18_gggga(x0, x1, x2, x3, x4)
U19_gggga(x0, x1, x2, x3, x4, x5)
U20_gggga(x0, x1, x2, x3, x4, x5)
appendcB_in_gga(x0, x1)
U21_gggga(x0, x1, x2, x3, x4)
U22_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U2_GGGGA(X1, X2, X3, X4, shanoicA_out_gggga(X1, X2, X4, X3, X6)) → SHANOIA_IN_GGGGA(X1, X3, X2, X4)
    The graph contains the following edges 1 >= 1, 5 > 1, 3 >= 2, 5 > 2, 2 >= 3, 5 > 3, 4 >= 4, 5 > 4

  • SHANOIA_IN_GGGGA(s(X1), X2, X3, X4) → SHANOIA_IN_GGGGA(X1, X2, X4, X3)
    The graph contains the following edges 1 > 1, 2 >= 2, 4 >= 3, 3 >= 4

  • SHANOIA_IN_GGGGA(s(X1), X2, X3, X4) → U2_GGGGA(X1, X2, X3, X4, shanoicA_in_gggga(X1, X2, X4, X3))
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4

(27) YES